\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $a$:ecl(${\it ds}$;${\it da}$), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$),\+
\\[0ex]$L$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex](\=$\forall$$L$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}normal($v$) \& ($\forall$$n$:$\mathbb{N}^{+}$. ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$v$)($n$,$L$) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($v$)))
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex]($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ \& ecl{-}halt(${\it ds}$;${\it da}$;$a$)($n$,${\it L'}$))
\\[0ex]$\Leftrightarrow$
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$v$)($n$,$L$))
\-\\[0ex]\& ($\forall$$m$:$\mathbb{N}$. ecl{-}act(${\it ds}$;${\it da}$;$m$;$a$)($L$) $\Leftrightarrow$ ecl{-}trans{-}act(${\it ds}$;${\it da}$;$v$)($m$,$L$)))
\-\\[0ex]$\Rightarrow$ ecl{-}halt(${\it ds}$;${\it da}$;$a$)(0,$L$)
\\[0ex]$\Rightarrow$ \=ecl{-}trans{-}state(reset{-}ecl{-}tuple($v$);$L$)\+
\\[0ex]$=$
\\[0ex]ecl{-}trans{-}init(reset{-}ecl{-}tuple($v$))
\\[0ex]$\in$ ecl{-}trans{-}type(reset{-}ecl{-}tuple($v$))
\-
\end{tabbing}